%\emph{Ownership} is useful for
%    analyzing runtime heap structure~\cite{mitchell:2006:runtime-ownership},
%    verification~\cite{DietlM2005}, %MuellerPoetzsch-Heffter99a
%    synchronization~\cite{BoyapatiLR2002}, % OOPSLA02
%    region-based memory management~\cite{BoyapatiSBR2003}, % PLDI03
%    and upgrades in persistent object stores~\cite{BoyapatiLS2003}. % POPL03

%\emph{Immutability} is useful in %modeling~\cite{BurdyEtAl05:STTT},
%    verification~\cite{TkachukD03},
%    compile- and run-time optimizations~\cite{Salcianu2006},
%    %Clausen97,PechtchanskiS2002,
%    refactoring~\cite{Fowler2000}, test input
%    generation~\cite{ArtziEGKPP2006}, regression oracle
%    creation~\cite{Xie2006}, %MarianiP2005
%    invariant detection~\cite{ErnstCGN2001:TSE}, specification
%    mining~\cite{DallmeierLWZ2006}, and program
%    comprehension~\cite{DoladoHOH2003}.

This paper presents \emph{Ownership Immutability Generic Java} (OIGJ),
    a simple and practical language extension
    that expresses both ownership and immutability information.
OIGJ is purely static, without any run-time representation.
This enables executing the resulting code on any JVM without run-time penalty.
Our ideas, though demonstrated using Java,
    are applicable to any statically typed language with generics,
    such as \CC, C\#, Scala, and Eiffel.

OIGJ follows the \emph{owner-as-dominator}
    discipline~\cite{Boyapati2004:PhD,ClarkeD2002,PotaninNCB2006}
    where an object cannot leak beyond its owner:
    outside objects cannot access it.
If an object owns
    its representation, then there are no aliases to its
    internal state.
For example, a \code{LinkedList} should own all its \code{Entry} objects
    (but not its elements); entries should not be exposed to clients, and
    entries from different lists must not be mixed.

The keyword \code{private} does not offer
    such strong protection as ownership, because
    a careless programmer might write a public method
    that exposes a private object (a.k.a.\ representation exposure).
Phrased differently, the name-based protection used in Java
    hides the variable but not the object,
    as opposed to ownership that ensures proper encapsulation.
The key idea in ownership is that representation objects
    are nested and encapsulated inside the objects to which they belong.
Because this nesting is transitive, this kind of ownership is also called
    \emph{deep} ownership~\cite{ClarkeW2003:ECOOP}.

OIGJ is based on our previous type systems for ownership (OGJ~\cite{PotaninNCB2006})
    and immutability (IGJ~\cite{ZibinPAAKE2007}).
Although ownership and immutability may seem like two unrelated concepts,
    a design involving both enhances
    the expressiveness of each individual concept.
On the one hand,
    immutability previously enhanced ownership by relaxing
    owner-as-dominator to owner-as-modifier~\cite{MuellerPoetzsch-Heffter99a}:
    it constrains modification instead of aliasing.
On the other hand, the benefits of adding ownership
    on top of immutability have not been investigated before.
One such benefit is easier creation of immutable cyclic data-structures
    by using ownership information.

Constructing an immutable object must be done with care.
An object begins in the \emph{raw} (not fully initialized) state and transitions to the \emph{cooked} state~\cite{BoylandRZ2009}
    when initialization is complete.
For an immutable object,
field assignment is allowed only when the object is \emph{raw},
    i.e., the object cannot be modified after it is \emph{cooked}.
An immutable object should not be visible to the outside world in its raw state
    because it would seem to be mutating.
% (and its invariants might not hold).
The challenge in building an immutable cyclic data-structure is that
    many objects must be raw simultaneously to create the cyclic structure.
Previous work restricted cooking an object to the constructor,
    i.e., an object becomes cooked when \underline{its} constructor finishes.

Our key observation is that
    \emph{an object can be cooked when \underline{its owner's} constructor finishes}.
More precisely, in OIGJ, a programmer can choose between cooking
    an object until its constructor finishes,
    or until its owner becomes cooked.
Because the object is encapsulated within its owner, the outside world
    will not see this cooking phase.
By adding ownership information, we can prolong the cooking time
    to make it easier to create complex data-structures.

Consider building an immutable \code{LinkedList} %from a given collection \code{c}
    (Sun's implementation is similar): % not exactly an excerpt, because Sun uses toArray()
    %  \code{LinkedList}

\begin{algorithmic}
\STATE \code{LinkedList(Collection<E> c)}
\STATE \code{\lb~this();}
\STATE \code{~~Entry<E> succ = this.header, pred = succ.prev;} %\myCOMMENT{predecessor}
\STATE \code{~~for (E e : c)}
\STATE \code{~~\lb~Entry<E> entry = new Entry<E>(e,succ,pred);}
\STATE \code{~~~~}\myCOMMENT{It is illegal to change an entry after it is cooked.}
\STATE \code{~~~~pred\underline{.next =} entry;~~pred = entry; \rb}
%\STATE \code{~~\rb}
\STATE \code{~~succ\underline{.prev =} pred;~\rb}
%\STATE \code{\rb}
\end{algorithmic}
An immutable list contains immutable entries, i.e.,
    the fields \code{next} and \code{prev} cannot be changed after an entry is cooked.
In IGJ and previous work on immutability, %lack ownership information, and therefore
    an object becomes cooked
    after \underline{its} constructor finishes.
Because \code{next} and \code{prev} are changed after that time,
    this code is illegal.
In contrast, in OIGJ, this code type-checks if we specify that
    the list (the \this object) owns all its entries (the entries are the list's representation).
The entries will become cooked when \underline{their owner's} (the list's) constructor finishes,
    thus permitting the underlined assignments during the list's construction.
%We stress that this mutation of the immutable entries is not visible to the outside world.
Therefore, there was no need to refactor the constructor of
    \code{LinkedList} for the benefit of OIGJ type-checking.

%    the entries must be linked to each other, however they cannot be modified
%    after being cooked.
%It is possible to refactor Sun's \code{LinkedList} to solve this problem
%    by recursively constructing the entries, however this solution is neither
%    intuitive nor efficient.
%The problem stems from the fact that the entries are treated as distinct objects,
%    and not as the representation of one single list.

% In IGJ, it is possible to create a cyclic data-structure
%    such as a bi-directional linked list,
%    but at a cost of major refactoring of Sun's
%    \code{LinkedList}~\cite{ZibinPAAKE2007}.

%Our key observation is that a constructor (that is building an immutable object)
%    may assign to any field in the object's representation}.
%    and therefore use \this as a safe under-approximation for the
%    object's representation.
%In OIGJ, the constructor may also assign to the fields of the objects owned by \this.


Informally, OIGJ provides the following ownership and immutability guarantees.
Let~$\Owner{o}$ denote the owner of~$o$ and let~$\Oprec$ denote the ownership tree,
    i.e.,
    the transitive, reflexive closure of~$o \Oprec \Owner{o}$.
Phrased differently, $\Owner{o}$ is the parent of $o$ in the tree,
    and the top (biggest) node in the tree is the root \World.
We say that $o_1$ is \emph{inside} $o_2$ iff $o_1 \Oprec o_2$,
    and it is \emph{strictly inside} if  $o_1 \neq o_2$.

%\indent\parbox{3in}{

\textbf{Ownership guarantee:}
    An object~$o'$ can point to object~$o$ iff~$o' \Oprec \Owner{o}$,
% Not true: todo{The explanation is not what the equation says; the equation says that$o'$ is owned by the owner of $o$ or by one of its owners.}
        i.e.,~$o$ is owned by~$o'$ or by one of its owners.
(This is the classical guarantee of \emph{owner-as-dominator}.) % as used in previous work.)

\textbf{Immutability guarantee:}
    An immutable object cannot be changed after it is cooked.
(When exactly an object becomes cooked is formally defined in \Ref{Section}{formal}.)
% LocalWords:  Scala OGJ IGJ succ pred prev iff
